Nuprl Lemma : es-causl-trans-test
11,40
postcript
pdf
es
:ES,
a
,
b
,
c
,
d
,
e
,
f
:E.
a
c
b
b
loc
c
(
c
<
d
)
d
c
e
e
c
f
(
a
<
f
)
latex
Definitions
P
Q
,
(
e
<
e'
)
,
e
loc
e'
,
e
c
e'
,
E
,
x
:
A
.
B
(
x
)
,
t
T
,
ES
Lemmas
es-causl
transitivity2
,
es-causl
transitivity1
,
es-causle
weakening
locl
,
es-causle
transitivity
,
event
system
wf
,
es-E
wf
,
es-causle
wf
,
es-le
wf
,
es-causl
wf
origin
es:ES, a, b, c, d, e, f:E. a c
b 
b loc c (c < d) d c e e c f (a < f) es:ES, a, b, c, d, e, f:E. a c b b loc c (c < d) d c e e c f (a < f) Qloc e' e'x:A. B(x)
T